\begin{tabbing}
$\forall$\=${\it es}$:ES, $e_{1}$:E, $e_{2}$:\{$e$:E$\mid$ loc($e$) $=$ loc($e_{1}$) $\in$ Id \}, $p$,\+
\\[0ex]$q$:(\{$e$:E$\mid$ loc($e$) $=$ loc($e_{1}$) $\in$ Id \}$\rightarrow$\{$e$:E$\mid$ loc($e$) $=$ loc($e_{1}$) $\in$ Id \}$\rightarrow$Prop).
\-\\[0ex](\=$\forall$$a$, $b$:\{$e$:E$\mid$ loc($e$) $=$ loc($e_{1}$) $\in$ Id \}.\+
\\[0ex]($a$ $\in$ [$e_{1}$, $e_{2}$]) $\Rightarrow$ ($b$ $\in$ [$e_{1}$, $e_{2}$]) $\Rightarrow$ ($p$($a$,$b$) $\Leftrightarrow$ $q$($a$,$b$)))
\-\\[0ex]$\Rightarrow$ ([$e_{1}$,$e_{2}$]$\sim$([$a$,$b$].$p$($a$,$b$))+ $\Leftrightarrow$ [$e_{1}$,$e_{2}$]$\sim$([$a$,$b$].$q$($a$,$b$))+)
\end{tabbing}